'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} Details: We have computed the following set of weak (innermost) dependency pairs: { max^#(L(x)) -> c_0() , max^#(N(L(0()), L(y))) -> c_1() , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} The usable rules are: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} The estimated dependency graph contains the following edges: {max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} ==> {max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} {max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} ==> {max^#(N(L(0()), L(y))) -> c_1()} {max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} ==> {max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} {max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} ==> {max^#(N(L(0()), L(y))) -> c_1()} We consider the following path(s): 1) { max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max^#(N(L(0()), L(y))) -> c_1()} The usable rules for this path are the following: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(0()), L(y))) -> c_1()} Details: We apply the weight gap principle, strictly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: Interpretation Functions: max(x1) = [1] x1 + [1] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] s(x1) = [1] x1 + [0] max^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [1] x1 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} and weakly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} Details: Interpretation Functions: max(x1) = [1] x1 + [6] L(x1) = [1] x1 + [2] N(x1, x2) = [1] x1 + [1] x2 + [12] 0() = [11] s(x1) = [1] x1 + [1] max^#(x1) = [1] x1 + [3] c_0() = [0] c_1() = [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [1] x1 + [9] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { max_1(4) -> 7 , max_1(8) -> 7 , max_1(10) -> 9 , max_1(12) -> 9 , L_0(2) -> 2 , L_0(2) -> 7 , L_0(2) -> 9 , L_1(2) -> 5 , L_1(7) -> 6 , L_1(9) -> 13 , N_0(2, 2) -> 2 , N_0(2, 2) -> 7 , N_0(2, 2) -> 9 , N_1(2, 2) -> 8 , N_1(5, 5) -> 10 , N_1(5, 6) -> 4 , N_1(5, 13) -> 12 , 0_0() -> 2 , 0_0() -> 7 , 0_0() -> 9 , s_0(2) -> 2 , s_0(2) -> 7 , s_0(2) -> 9 , s_1(9) -> 7 , s_1(9) -> 9 , max^#_0(2) -> 1 , max^#_1(4) -> 3 , max^#_1(10) -> 11 , max^#_1(12) -> 11 , c_1_0() -> 1 , c_1_1() -> 3 , c_1_1() -> 11 , c_2_0(1) -> 1 , c_2_1(11) -> 3 , c_2_1(11) -> 11 , c_3_1(3) -> 1} 2) { max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} The usable rules for this path are the following: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} Details: We apply the weight gap principle, strictly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: Interpretation Functions: max(x1) = [1] x1 + [1] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] s(x1) = [1] x1 + [0] max^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [1] x1 + [3] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} and weakly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y))))} Details: Interpretation Functions: max(x1) = [1] x1 + [0] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [1] s(x1) = [1] x1 + [2] max^#(x1) = [1] x1 + [12] c_0() = [0] c_1() = [0] c_2(x1) = [1] x1 + [0] c_3(x1) = [1] x1 + [11] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max^#(N(L(s(x)), L(s(y)))) -> c_2(max^#(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { max_1(4) -> 7 , max_1(8) -> 7 , max_1(10) -> 9 , max_1(12) -> 9 , L_0(2) -> 2 , L_0(2) -> 7 , L_0(2) -> 9 , L_1(2) -> 5 , L_1(7) -> 6 , L_1(9) -> 13 , N_0(2, 2) -> 2 , N_0(2, 2) -> 7 , N_0(2, 2) -> 9 , N_1(2, 2) -> 8 , N_1(5, 5) -> 10 , N_1(5, 6) -> 4 , N_1(5, 13) -> 12 , 0_0() -> 2 , 0_0() -> 7 , 0_0() -> 9 , s_0(2) -> 2 , s_0(2) -> 7 , s_0(2) -> 9 , s_1(9) -> 7 , s_1(9) -> 9 , max^#_0(2) -> 1 , max^#_1(4) -> 3 , max^#_1(10) -> 11 , max^#_1(12) -> 11 , c_2_0(1) -> 1 , c_2_1(11) -> 3 , c_2_1(11) -> 11 , c_3_1(3) -> 1} 3) { max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(0()), L(y))) -> c_1()} The usable rules for this path are the following: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z)))))) , max^#(N(L(0()), L(y))) -> c_1()} Details: We apply the weight gap principle, strictly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: Interpretation Functions: max(x1) = [1] x1 + [1] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] s(x1) = [1] x1 + [0] max^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))} and weakly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))} Details: Interpretation Functions: max(x1) = [1] x1 + [1] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [1] 0() = [1] s(x1) = [1] x1 + [3] max^#(x1) = [1] x1 + [2] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max^#(N(L(0()), L(y))) -> c_1()} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { max_1(4) -> 7 , max_1(8) -> 7 , max_1(10) -> 9 , L_0(2) -> 2 , L_0(2) -> 7 , L_0(2) -> 9 , L_1(2) -> 5 , L_1(7) -> 6 , L_1(9) -> 5 , N_0(2, 2) -> 2 , N_0(2, 2) -> 7 , N_0(2, 2) -> 9 , N_1(2, 2) -> 8 , N_1(5, 5) -> 10 , N_1(5, 6) -> 4 , 0_0() -> 2 , 0_0() -> 7 , 0_0() -> 9 , s_0(2) -> 2 , s_0(2) -> 7 , s_0(2) -> 9 , s_1(9) -> 7 , s_1(9) -> 9 , max^#_0(2) -> 1 , max^#_1(4) -> 3 , c_1_0() -> 1 , c_1_1() -> 3 , c_3_1(3) -> 1} 4) {max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} The usable rules for this path are the following: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z)))))} We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs. 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y , max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Details: We apply the weight gap principle, strictly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: Interpretation Functions: max(x1) = [1] x1 + [1] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [0] s(x1) = [1] x1 + [0] max^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [1] Finally we apply the subprocessor We apply the weight gap principle, strictly orienting the rules {max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))} and weakly orienting the rules { max(L(x)) -> x , max(N(L(0()), L(y))) -> y} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y))))} Details: Interpretation Functions: max(x1) = [1] x1 + [0] L(x1) = [1] x1 + [0] N(x1, x2) = [1] x1 + [1] x2 + [0] 0() = [11] s(x1) = [1] x1 + [6] max^#(x1) = [1] x1 + [0] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [1] x1 + [0] Finally we apply the subprocessor 'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment'' ------------------------------------------------------------------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: The problem was solved by processor 'Bounds with default enrichment': 'Bounds with default enrichment' -------------------------------- Answer: YES(?,O(n^1)) Input Problem: innermost relative runtime-complexity with respect to Strict Rules: { max(N(L(x), N(y, z))) -> max(N(L(x), L(max(N(y, z))))) , max^#(N(L(x), N(y, z))) -> c_3(max^#(N(L(x), L(max(N(y, z))))))} Weak Rules: { max(N(L(s(x)), L(s(y)))) -> s(max(N(L(x), L(y)))) , max(L(x)) -> x , max(N(L(0()), L(y))) -> y} Details: The problem is Match-bounded by 1. The enriched problem is compatible with the following automaton: { max_1(4) -> 7 , max_1(8) -> 7 , max_1(10) -> 9 , L_0(2) -> 2 , L_0(2) -> 7 , L_0(2) -> 9 , L_1(2) -> 5 , L_1(7) -> 6 , L_1(9) -> 5 , N_0(2, 2) -> 2 , N_0(2, 2) -> 7 , N_0(2, 2) -> 9 , N_1(2, 2) -> 8 , N_1(5, 5) -> 10 , N_1(5, 6) -> 4 , 0_0() -> 2 , 0_0() -> 7 , 0_0() -> 9 , s_0(2) -> 2 , s_0(2) -> 7 , s_0(2) -> 9 , s_1(9) -> 7 , s_1(9) -> 9 , max^#_0(2) -> 1 , max^#_1(4) -> 3 , c_3_1(3) -> 1} 5) {max^#(L(x)) -> c_0()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: max(x1) = [0] x1 + [0] L(x1) = [0] x1 + [0] N(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] s(x1) = [0] x1 + [0] max^#(x1) = [0] x1 + [0] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {max^#(L(x)) -> c_0()} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {max^#(L(x)) -> c_0()} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {max^#(L(x)) -> c_0()} Details: Interpretation Functions: max(x1) = [0] x1 + [0] L(x1) = [1] x1 + [0] N(x1, x2) = [0] x1 + [0] x2 + [0] 0() = [0] s(x1) = [0] x1 + [0] max^#(x1) = [1] x1 + [1] c_0() = [0] c_1() = [0] c_2(x1) = [0] x1 + [0] c_3(x1) = [0] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {max^#(L(x)) -> c_0()} Details: The given problem does not contain any strict rules